atoms-distinct(tab) == i, j:{0..||tab|| }. (st-atom(tab;i) = st-atom(tab;j))  (i = j) 

latex

---

clarification:

atoms-distinct(tab)
== i:{0..||tab|| }, j:{0..||tab|| }.
== (st-atom(tab;i) = st-atom(tab;j)  Atom1)  (i = j  ) 

latex

Definitions	x:A. B(x), {i..j}, #$n, ||tab|| , P  Q, Atom$n, st-atom(tab;n), s = t,
FDL editor aliases	st-atoms-distinct